Lambda the Ultimate

Here's an interesting paper recently mention in another thread: Total Functional Programming...

Abstract: The driving idea of functional programming is to make programming more closely related to mathematics. A program in a functional language such as Haskell or Miranda consists of equations which are both computation rules and a basis for simple algebraic reasoning about the functions and data structures they define. The existing model of functional programming, although elegant and powerful, is compromised to a greater extent than is commonly recognized by the presence of partial functions. We consider a simple discipline of total functional programming designed to exclude the possibility of non-termination. Among other things this requires a type distinction between data, which is finite, and codata, which is potentially infinite.

I presume that the bogus definiton of "fib" is a subtle reminder of the importance of eliminating bottom.

Ott—a tool for writing definitions of programming languages and calculi.

Ott is a tool for writing definitions of programming languages and calculi. It takes as input a definition of a language syntax and semantics, in a concise and readable ASCII notation that is close to what one would write in informal mathematics. It generates LaTeX to build a typeset version of the definition, and Coq, HOL, and Isabelle versions of the definition. Additionally, it can be run as a filter, taking a LaTeX/Coq/Isabelle/HOL source file with embedded (symbolic) terms of the defined language, parsing them and replacing them by target-system terms. For a simple example, here is an Ott source file for an untyped call-by-value lambda calculus (test10.ott), and the generated LaTeX (compiled to pdf) and (compiled to ps), Coq, Isabelle, and HOL definitions.

Most simply, the tool can be used to aid completely informal LaTeX mathematics. Here it permits the definition, and terms within proofs and exposition, to be written in a clear, editable, ASCII notation, without LaTeX noise. It generates good-quality typeset output. By parsing (and so sort-checking) this input, it quickly catches a range of simple errors, e.g. inconsistent use of judgement forms or metavariable naming conventions.

That same input can be used to generate formal definitions, for Coq, HOL, and Isabelle. It should thereby enable a smooth transition between use of informal and formal mathematics. Additionally, the tool can automatically generate definitions of functions for free variables, single and multiple substitutions, subgrammar checks (e.g. for value subgrammars), and binding auxiliary functions. (At present only a fully concrete representation of binding is supported, without quotienting by alpha equivalence.)

The distribution includes several examples, in varying levels of completeness: untyped and simply typed lambda-calculus, a calculus with ML polymorphism, the POPLmark Fsub with and without records, an ML module system taken from (Leroy, JFP 1996) and equipped with an operational semantics, and LJ, a lightweight Java fragment.

Peter Sewell and his team continue to bridge the gap between the informal and formal worlds of programming language semantics.

Anders Hejlsberg, Herb Sutter, Erik Meijer, Brian Beckman: Software Composability and the Future of Languages

This is an about an hour long video on channel9 about various .NET languages.

http://channel9.msdn.com/Showpost.aspx?postid=273697

Extremely attractive overview and slides about a one-hour Erlang talk by André Pang at linux.conf.au 2007.

I gave a talk titled Concurrency and Erlang at Linux.conf.au in January, 2007. Thank you so much to everybody who attended it and made me feel welcome: I got overwhelmingly positive feedback from it, and it was an honour to speak at such an esteemed conference.

Another reason I wish I'd talked myself into attending this conference!

Chris Oliver has been working on F3 ("form follows function"), a new scripting language for the java platform. Here is a detailed description of F3's features.

It is already in heavy development but not yet released, and there are plugins for both Netbeans and Eclipse. Some of its functionality and the examples Chris has shared indicate it could be an alternative to Flash and processing.

Summary of some of its features:

• It is case-sensitive and uses curly braces, so it is very java-like.
• It is statically typed with type inference (like boo). It uses "var" for type inferenced declarations (var x = 3;), like in groovy or C# 3.0.
• It supports a JSON-like declarative syntax for building GUIs (as opposed to XML or YAML).
• Has a ".." range literal: var result = sum([1,3..100]);
• Supports SQL notation for querying arrays:

  var squares = select n*n from n in [1..100];
  //another example:
  var titleTracks =
              select indexof track + 1 from album in albums,
                        track in album.tracks
                            where track == album.title; // yields [1,4]
  

• You can also embed the JSON-like syntax in code (or vice-versa):

          var chris = Person {
               name: "Chris"
               children:
               [Person {
                   name: "Dee"
               },
               Person {
                   name: "Candice"
               }]
         };
  

• Supports expressions inside strings:

  var answer = true;
  var s = "The answer is {if answer then "Yes" else "No"}"; // s = 'The answer is Yes'
  

• Supports "do" or "do later" for code that either allows background events to occur or runs in a background thread itself:

          import java.lang.System;
          var saying1 = "Hello World!";
          var saying2 = "Goodbye Cruel World!";
          do later {
               System.out.println(saying1);
          }
          System.out.println(saying2);
  

• It may be using a MultiVM technique where different applications run in the same JVM instance, saving memory and improving start-up time.
• All methods and attributes of a class have to be declared first (like in C and C++, yay), and then the implementations are written outside the class body (like in nice).
• Instead of constructors and setters, F3 uses "triggers":

           import java.lang.System;
           class X {
                attribute nums: Number*;
           }
           trigger on new X {
                insert [3,4] into this.nums;
           }
           var x = new X();
           System.out.println(x.nums == [3,4]); // prints true
  

The second draft of R6RS, version 5.92, is now available at www.r6rs.org. (For more general information about Scheme standards, see the Standards page at schemers.org.)

This version of R6RS incorporates the responses to the formal comments that were submitted prior to Nov 15th, 2006. A few of the changes are highlighted below (not intended to be comprehensive):

• The report has been split into two separate documents: one for the base language, and one for the standard libraries. (A third document is currently planned, to include certain non-normative appendices.)
• The I/O system has been significantly revised.
• A number of features have been dropped from the report, including the inexact arithmetic library and the declarations feature.
• The report now includes a formal operational semantics, developed by Robby Findler and Jacob Matthews, building on their semantics for R5RS.
• "Top-level programs" replace scripts in the base language, eliminating certain OS-specificities, with a specification for scripts to be added in a non-normative appendix.

The current six-month public comment period is still ongoing, and will continue until March 15, 2007. The schedule subsequent to that date can be found here.

The editors encourage comments on the report, either informally on the discuss@r6rs.org mailing list, or via the formal comment process.

Of course, kibitzing here on LtU is welcome too! (Previous discussions on LtU include the announcement of the previous draft and the June status report.)

Locus Solum: From the rules of logic to the logic of rules by Jean-Yves Girard, 2000.

The monograph below has been conceived as the project of giving reasonable foundations to logic, on the largest possible grounds, but not with the notorious reductionist connotation usually attached to "foundations". Locus Solum would like to be the common playground of logic, independent of systems, syntaxes, not to speak of ideologies. But wideness of scope is nothing here but the reward of sharpness of concern : I investigate the multiple aspects of a single artifact, the design. Designs are not that kind of syntax-versus-semantics whores that one can reshape according to the humour of the day : one cannot tamper with them, period. But what one can achieve with them, once their main properties —separation, associativity, stability— have been understood, is out of proportion with their seemingly banal definition.

Sounds rather controversial, but can make an interesting reading if you believe logic is related to programming (your last name doesn't have to be either Curry or Howard).

Another entry for HOPL-III that is an interesting account of The Evolution of Lua by Roberto Ierusalimschy, Luiz Henrique de Figueiredo and Waldemar Celes.

We report on the birth and evolution of Lua, and discuss how Lua moved from a simple configuration language to a versatile, widely used language that supports extensible semantics, anonymous functions, full lexical scoping, proper tail calls, and coroutines.

The paper is timely for me, since I recently acquired the book "Programming in Lua V2" and am slowly trying to learn the language. It's hard not to like the model of language evolution taken by the Lua community. Lua has actively staked the ground of an embeddable scripting language, having simplicity and size as a major focus, and a very active two way street between embedded scripting language and host language C. The paper provides a good accounting of many of the design decisions made through the history of versions, though I would have liked a bit more mention of the decision to go with a register based VMs.

Overall, I'd rate it as a very good read for those that are interested in PL design. Other papers from HOPL-III mentioned on LtU: Haskell and AppleScript.

Pivotal is a document-centered presentation of Haskell. It aims to provide a user-friendly environment in which Haskell documents can be interactively developed and manipulated. A Haskell document is essentially an ordinary Haskell module that may also include free-standing Haskell expressions. When a document is displayed, the values of any such expressions are evaluated and displayed in-place.

Think of a document containing code, comments, and examples, all presented in an aesthetically pleasing manner. The document is live, so you can make changes and see them immediately. This reminds me somewhat of the Lab system in J: interactive tutorials that allow the user to experiment after each new point is presented.

Beauty in the Beast by Wouter Swierstra, Thorsten Altenkirch. 2006.

We provide a functional specification of three central components of Simon Peyton Jones’s awkward squad: teletype I/O, mutable state and concurrency. By constructing an internal model of such concepts within our programming language, we can reason about programs that perform I/O as if they were pure functions. One important application of our approach is accommodating I/O in a dependently typed programming language.